e sends || a == e':E. (isrcv(e'))  (sender(e') = e)  val(e'):valtype(e')||a 

latex

---

clarification:

es-send-atom(es;e;a)
== e':es-E(es).
== (es-isrcv(es; e'))
==  (es-sender(es; e') = e  es-E(es))
==  free-from-atom{1}(es-valtype(es; e');es-val(es; e');a) 

latex

Definitions	x:A. B(x), b, isrcv(e), P  Q, s = t, E, sender(e), x:T||a, valtype(e), val(e)
FDL editor aliases	es-send-atom